module MeteoCal

//signatures

//abstract user may be event publishers and event participants
sig Calendar{
		owner: one User,
		events: set Event
}

sig User{
	calendar: one Calendar
}

sig InvitedUser extends User{
		acceptEvent: lone Event,
		declineEvent: lone Event
}

sig Event{
		publisher: one User,
		participant: set User,
		
}

sig CreateEvent{	
		create: set Event,
		publisher: one User,
		invite: set InvitedUser
}

//the situation of delete event is quite similar to update event
sig UpdateEvent{
		update: set Event,
		publisher: one User
}


sig ViewEvent{
		view: set Event,
		viewer: set User
}

sig ViewUser{
		view: one User,
		viewer: one User
}


//facts

fact User{
//the calendar belongs to one user
		all u: User | u = u.calendar.owner
}

fact Calendar{
//The user should be the publisher or participant of the event which in his calendar
		all c: Calendar | c.owner = c.events.publisher or c.owner = c.events.participant
}

fact EventProperties{
//the event publisher won't be the participant of this event. (Event)
		no e: Event | e.publisher in e.participant
}

fact InvitedUserProperties{
//The inviteduser can't accept or decline the event which was published by himself.
		no i: InvitedUser | i = i.acceptEvent.publisher
		no i: InvitedUser | i = i.declineEvent.publisher
// the inviteduser can't only do one action of event either decline or accept but need to do one time
		no i: InvitedUser | i.acceptEvent = i.declineEvent
// the inviteduser can't be the participant of the event if declined to this event
		no i: InvitedUser | i in i.declineEvent.participant
//the inviteduser will be the participant of the event if accept to this event
		all i: InvitedUser | i = i.acceptEvent.participant
}

fact CreateEventProperties{
//The user who is a publisher won't invete himself/herself. (CreateEvent)
		no c: CreateEvent | c.publisher in c.invite
//The user who is a publisher won't accept and decline the event
		no c: CreateEvent | c.publisher = c.create.participant

		all c: CreateEvent | c.publisher = c.create.publisher

}

fact UpdateEventProperties{
//The user who can update the event is the owner of this event
		all e: UpdateEvent | e.publisher = e.update.publisher
}

fact ViewUser{}



pred show {}
 run show for 3 but exactly 3 Event, 3 User, 2 InvitedUser, 1 ViewUser
